(declare-fun a () String)
(assert (= (str.len a) 3))
(push)
(assert (= 0 (str.indexof a "abc" 0)))
(check-sat)
(pop)
(assert (= 0 (str.indexof a "abc" 0)))
(push)
(check-sat)
